/LMAR=0/XLINE=3/FONT#0=BASL30/FONT#1=BASI30/FONT#2=BASB30/FONT#5=SUP/FONT#3=STA200/FONT#4=NGB25
␈↓ ↓H␈↓␈↓βS␈↓∧ Artificial Intelligence Laboratory, STANFORD UNIVERSITY, Stanford, California 94305
␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ 	oOctober 29, 1975








␈↓ ↓H␈↓Letter in Support of
␈↓ ↓H␈↓Recommendation for Appointment to the Faculty
␈↓ ↓H␈↓David C. Luckham, Adjunct Professor



␈↓ ↓H␈↓As␈α~required␈α~by␈α~the␈α~Procedures␈α~for␈α~Recommending␈α~Appointments,␈α≠Reappointments,␈α~and
␈↓ ↓H␈↓Promotions␈α⊂in␈α⊂the␈α⊂Stanford␈α⊂Faculty,the␈α⊂enclosed␈α⊂documents␈α⊂-␈α⊂Summary␈α⊂of␈α⊂Experience␈α⊂Record,
␈↓ ↓H␈↓Letters␈α
of␈α
Recommendation,␈α
and␈α
Comments␈α
on␈α
the␈α
Publications␈α
of␈α
D.C.␈α
Luckham␈α
-␈α∞provide␈α
the
␈↓ ↓H␈↓largest part of the information requested.The following comments complete the dossier.

␈↓ ↓H␈↓I. Area of work

␈↓ ↓H␈↓Dr.␈α
Luckham␈α∞came␈α
to␈α
Stanford␈α∞as␈α
a␈α
Research␈α∞Associate␈α
in␈α
Computer␈α∞Science␈α
in␈α
1968␈α∞and␈α
then
␈↓ ↓H␈↓went␈α
to␈α
UCLA␈αas␈α
Associate␈α
Professor␈αof␈α
Computer␈α
Science␈αin␈α
1971.␈α
His␈αreason␈α
for␈α
returning␈αto
␈↓ ↓H␈↓Stanford,␈α∃and␈α∃accepting␈α∃what␈α∃amounts␈α∃to␈α∃a␈α∃demotion␈α∃in␈α∃rank,␈α∃was␈α∃the␈α∃superior␈α∃research
␈↓ ↓H␈↓environment␈α
of␈α∞the␈α
Stanford␈α∞Arti≡cial␈α
Intelligence␈α∞Laboratory␈α
both␈α∞in␈α
terms␈α∞of␈α
facilities␈α∞and␈α
in
␈↓ ↓H␈↓the quality of students with whom he could work.

␈↓ ↓H␈↓While␈αhere␈αhe␈αhas␈αcontinued␈αhis␈αresearch␈αin␈αautomatic␈αtheorem␈αproving␈αand␈αmathematical␈α
theory
␈↓ ↓H␈↓of computation and started a new e≥ort in automatic programming.

␈↓ ↓H␈↓If␈αhis␈αpromotion␈αto␈αAdjunct␈αProfessor␈αis␈αapproved,␈αhe␈αwill␈αcontinue␈αhis␈αpersonal␈αresearch␈αactivity
␈↓ ↓H␈↓and␈αwill␈αplay␈αa␈αstill␈αmore␈αactive␈αrole␈αin␈αthe␈αsupervision␈αof␈αgraduate␈αstudents␈αsince␈αhe␈αwill␈αbe␈αable
␈↓ ↓H␈↓to␈αserve␈αas␈αa␈αprincipal␈α
dissertation␈αadviser.␈αHe␈αwill␈αalso␈αbe␈α
able␈αto␈αapply␈αfor␈αresearch␈α
support␈αin
␈↓ ↓H␈↓his␈αown␈αname␈αas␈αprincipal␈αinvestigator,␈αand␈αthis␈αwill␈αrelieve␈αthe␈αDirector␈αfrom␈αhaving␈αto␈αserve␈αas
␈↓ ↓H␈↓formal␈α∞principal␈α∞investigator␈α∞in␈α∞some␈α∞cases␈α
and␈α∞will␈α∞enable␈α∞Luckham's␈α∞part␈α∞of␈α∞the␈α
Laboratory's
␈↓ ↓H␈↓work to stand on its own feet.

␈↓ ↓H␈↓II. Justi≡cation of Promotion

␈↓ ↓H␈↓The␈αprimary␈αjusti≡cation␈αfor␈αpromoting␈αDavid␈αLuckham␈αto␈αAdjunct␈αProfessor␈αis␈αthe␈αquality␈αand
␈↓ ↓H␈↓quantity␈α
of␈α
his␈αcontinuing␈α
scienti≡c␈α
work.␈αHis␈α
early␈α
work␈αin␈α
program␈α
schemas␈αhas␈α
stood␈α
the␈αtest␈α
of
␈↓ ↓H␈↓time␈αand␈α
is␈αstill␈αreferred␈α
to␈αquite␈α
often.␈αHe␈αcontinues␈α
in␈αa␈αleading␈α
position␈αin␈α
automatic␈αtheorem
␈↓ ↓H␈↓proving␈α∀and␈α∃is␈α∀almost␈α∃alone␈α∀in␈α∀successfully␈α∃applying␈α∀automatic␈α∃theorem␈α∀proving␈α∃to␈α∀actual
␈↓ ↓H␈↓mathematical␈αproblems,␈αalbeit␈αin␈αa␈αlimited␈αdomain␈αof␈αmathematics␈αfor␈αwhich␈αthe␈αpresent␈αmethods
␈↓ ↓H␈↓are␈α
suitable.␈α
Recently␈α
he␈α
has␈α
started␈α
new␈α
e≥orts␈α
in␈α
developing␈α
systems␈α
for␈α
proving␈αassertions␈α
about
␈↓ ↓H␈↓computer␈α
programs␈α
incorporating␈αhis␈α
previous␈α
programs␈α
for␈αautomatic␈α
theorem␈α
proving.␈α
In␈αthis,
␈↓ ↓H␈↓he is occupying a leading postion in what has become a very competitive ≡eld.
␈↓ ↓H␈↓α␈↓ ¬]October 29, 1975␈↓ 
nPage 2␈↓ 


␈↓ ↓H␈↓Most␈α∩recently␈α∩he␈α∪has␈α∩started␈α∩an␈α∩e≥ort␈α∪in␈α∩automatice␈α∩programming,␈α∩i.e.,␈α∪generating␈α∩computer
␈↓ ↓H␈↓programs␈α⊃automatically␈α⊃from␈α⊃speci≡cations␈α⊃of␈α⊂the␈α⊃desired␈α⊃performance.␈α⊃There␈α⊃is␈α⊃a␈α⊂substantial
␈↓ ↓H␈↓probability of this work obtaining independent support if we promote him to Adjunct Professor.

␈↓ ↓H␈↓III. The Candidate's Role

␈↓ ↓H␈↓With␈αreference␈α
to␈αthe␈α
above␈α(which␈αis␈α
listed␈αas␈α
IV.␈αin␈αthe␈α
procedures),␈αthe␈α
following␈αis␈αin␈α
response
␈↓ ↓H␈↓to␈α∞Paragraphs␈α∞A.␈α∞through␈α∞C.;␈α∞Paragraph␈α∞D.␈α∞is␈α∞covered␈α∞in␈α∞the␈α∞Summary␈α∞of␈α∞Experience␈α∞Record.
␈↓ ↓H␈↓Since␈α∞September␈α
1971,␈α∞David␈α∞Luckham␈α
as␈α∞been␈α
a␈α∞Research␈α∞Computer␈α
Scientist␈α∞in␈α∞the␈α
Arti≡cial
␈↓ ↓H␈↓Intelligence␈α∩Laboratory.␈α⊃He␈α∩has␈α⊃been␈α∩the␈α⊃instigator␈α∩and␈α⊃leader␈α∩of␈α⊃all␈α∩our␈α⊃work␈α∩in␈α⊃computer
␈↓ ↓H␈↓theorem␈αproving␈αand␈αmuch␈αof␈αour␈αwork␈αin␈αprogram␈αveri≡cation.␈αBoth␈αof␈αthese␈αareas␈αare␈αessential
␈↓ ↓H␈↓for␈α
arti≡cial␈α
intelligence␈α
research␈α
and␈α
for␈α∞mathematical␈α
theory␈α
of␈α
computation␈α
and,␈α
as␈α∞shown␈α
by
␈↓ ↓H␈↓the␈α
letters,␈α
David␈α
Luckham␈α
has␈αcontributed␈α
strongly␈α
to␈α
the␈α
Laboratory's␈α
international␈αreputation
␈↓ ↓H␈↓in␈α∂these␈α∞areas␈α∂and␈α∞presumably␈α∂to␈α∞the␈α∂continuation␈α∞of␈α∂our␈α∞government␈α∂support.Besides␈α∂this,␈α∞his
␈↓ ↓H␈↓area␈α∞has␈α∂attracted␈α∞quite␈α∂a␈α∞few␈α∂graduate␈α∞students␈α∞whose␈α∂dissertation␈α∞work␈α∂he␈α∞has␈α∂ably␈α∞directed.
␈↓ ↓H␈↓His␈α∞ability␈α∞to␈α∂conceive␈α∞and␈α∞organize␈α∞independent␈α∂research␈α∞projects␈α∞that␈α∞can␈α∂attract␈α∞government
␈↓ ↓H␈↓support␈αhas␈αbeen␈αdemonstrated␈αand␈αit␈αis␈αregarded␈αas␈αanomalous␈αthat␈αhe␈αdoes␈αnot␈αyet␈αhave␈αa␈αtitle
␈↓ ↓H␈↓allowing him to be a principal investigator.

␈↓ ↓H␈↓We␈αexpect␈αhim␈αto␈αbe␈αsuccessful␈αin␈αthe␈αfuture,␈αbecause␈αhe␈αhas␈αalready␈αbeen␈αsuccessful␈αin␈αthis␈αrole.
␈↓ ↓H␈↓However, his status must match his role if we are to be fair or are to keep him.

␈↓ ↓H␈↓His departmental activities outside his research are listed.

␈↓ ↓H␈↓While␈α⊂his␈α∂position␈α⊂is␈α∂not␈α⊂primarily␈α∂as␈α⊂a␈α∂teacher,␈α⊂we␈α∂expect␈α⊂that␈α∂he␈α⊂will␈α∂occasionally␈α⊂teach␈α∂an
␈↓ ↓H␈↓advanced course and direct seminars. He does this adequately.

␈↓ ↓H␈↓This␈α∩is␈α⊃primarily␈α∩a␈α⊃matter␈α∩of␈α⊃making␈α∩the␈α⊃title␈α∩match␈α⊃the␈α∩function,␈α⊃the␈α∩candidate␈α∩is␈α⊃already
␈↓ ↓H␈↓performing.␈αThe␈αletters␈αsoliciting␈αopinions␈αasked␈αfor␈αcomparison␈αwith␈αother␈αoutstanding␈αpeople␈αin
␈↓ ↓H␈↓the ≡eld with the excellent results evidenced in the letters.


␈↓ ↓H␈↓Sincerely,



␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Director
␈↓ ↓H␈↓Professor of Computer Science